i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da), j:Id.
msg-spec-loc(snd; i)
 sqequal(R-has-loc(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd); j); eq_id(i; j)) 

latex

Definitions

P  Q, guard(T), sq_type(T), True, T, Y, P  Q, P  Q, P  Q, reduce(f; k; as), b, band(p; q), if b then t else f fi , prop{i:l}, tt, x. t(x), subtype(S; T), top, t  T, R-state-var-init(i; ds; da; x; T; v; ks; tr), bor(p; q), ff, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), R-has-loc(R; i), P  Q, x:A. B(x), decidable(P), False, A, msg-spec-loc(snd; i), Unit, x(s), ecl-trans-tuple{i:l}(ds; da), , update-spec(ds; da),

Lemmas

cons member, decidable equal IdLnk, decidable l member, Id sq, ecl-tags wf, band wf, true wf, squash wf, bor wf, lsrc wf, bfalse wf, assert of null, update-spec-vars wf, null wf3, member-remove-repeats, IdLnk wf, msg-spec-links wf, idlnk-deq wf, remove-repeats wf, l member wf, Knd wf, ecl wf, msg-spec wf, update-spec wf, Id wf, msg-spec-loc wf, bool sq, ecl-machine3-loc, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, btrue wf, assert-eq-id, eqtt to assert, assert wf, iff transitivity, bool wf, eq id wf, fpf wf, pi2 wf, id-deq wf, fpf-cap wf, pi1 wf, ma-valtype wf, decl-state wf, nat wf, fpf-trivial-subtype-top, ecl-machine2-loc, top wf, R-state-var-loc, ecl-trans-tuple wf, ecl-trans wf